T:Type, t:T, p:FinProbSpace, l:IdLnk, ds:x:Id fp Type, P:(State(ds)),
f:({s:State(ds)| (P(s))} OutcomeT).
Normal(ds)  (weakPrecondSendR2{a:ut2, tg:ut2}(T; t; p; l; ds; P; f)  Realizer) 

latex

Definitions

Type, t  T, ||as||, a < b, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , {i..j}, Void, x:AB(x), x:A. B(x), , (x  l), #$n, r  s, x. t(x), xL. P(x), l[i], a  j < b. E(j), s = t, x:A  B(x), type List, Id, FinProbSpace, IdLnk, , State(ds), a:A fp B(a), Outcome, f(a), b, Normal(ds), xdom(f). v=f(x)   P(x;v), Atom$n, Top, IdDeq, f(x)?z, , b, , P  Q, Unit, left + right, if b then t else f fi , "$x", DeclaredType(ds;x), [car / cdr], [], x : v, x.A(x), x:A.B(x), <a, b>, Rsends(ds;knd;T;l;dt;g), Rsframe(lnk;tag;L), locl(a), Rpre(loc;ds;a;p;P), Realizer, Knd, source(l), weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f)

Lemmas

Rlist wf, lsrc wf, Knd wf, es realizer wf, Rpre wf, locl wf, Rsframe wf, Rsends wf, fpf-single wf, decl-type wf, ifthenelse wf, fpf-cap-single1, fpf-cap-single, eqof eq btrue, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, le wf, length wf nat, nat wf, fpf-cap wf, id-deq wf, top wf, normal-ds wf, assert wf, p-outcome wf, decl-state wf, bool wf, Id wf, rationals wf, qsum wf, length wf1, select wf, int seg wf, l all wf2, qle wf, int inc rationals, l member wf